Left Termination of the query pattern
insert(a,g,a)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

insert(X, void, tree(X, void, void)).
insert(X, tree(X, Left, Right), tree(X, Left, Right)).
insert(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), insert(X, Left, Left1)).
insert(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), insert(X, Right, Right1)).
less(0, s(X1)).
less(s(X), s(Y)) :- less(X, Y).

Query: insert(a,g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="H: insert(T1, T2, T3)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | insert(T1, void, T3), SCOPE: 1, CLAUSE: 1 | insert(T1, void, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, void, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT2 is ground\nX3 is free\ninsert(T1, T2, T3) !=? insert(X3, void, tree(X3, void, void))", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: insert(T1, void, T3), SCOPE: 1, CLAUSE: 1 | insert(T1, void, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, void, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: insert(T1, void, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, void, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: insert(T1, void, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true | insert(T1, tree(T12, T13, T14), T3), SCOPE: 1, CLAUSE: 2 | insert(T1, tree(T12, T13, T14), T3), SCOPE: 1, CLAUSE: 3\n\nT12 is ground\nT13 is ground\nT14 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT2 is ground\nX3 is free\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, T2, T3) !=? insert(X3, void, tree(X3, void, void))\ninsert(T1, T2, T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: insert(T1, tree(T12, T13, T14), T3), SCOPE: 1, CLAUSE: 2 | insert(T1, tree(T12, T13, T14), T3), SCOPE: 1, CLAUSE: 3\n\nT12 is ground\nT13 is ground\nT14 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(less(T25, T21), insert(T25, T22, T26)) | insert(T1, tree(T21, T22, T23), T3), SCOPE: 1, CLAUSE: 3\n\nT21 is ground\nT22 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: insert(T1, tree(T12, T13, T14), T3), SCOPE: 1, CLAUSE: 3\n\nT12 is ground\nT13 is ground\nT14 is ground\nX28 is free\nX29 is free\nX30 is free\nX31 is free\nX32 is free\ninsert(T1, tree(T12, T13, T14), T3) !=? insert(X28, tree(X29, X30, X31), tree(X29, X32, X31))", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(less(T25, T21), insert(T25, T22, T26)), SCOPE: 2, CLAUSE: 4 | ','(less(T25, T21), insert(T25, T22, T26)), SCOPE: 2, CLAUSE: 5 | ?_2 | insert(T1, tree(T21, T22, T23), T3), SCOPE: 1, CLAUSE: 3\n\nT21 is ground\nT22 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(less(T25, T21), insert(T25, T22, T26)), SCOPE: 2, CLAUSE: 4\n\nT21 is ground\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(less(T25, T21), insert(T25, T22, T26)), SCOPE: 2, CLAUSE: 5 | ?_2 | insert(T1, tree(T21, T22, T23), T3), SCOPE: 1, CLAUSE: 3\n\nT21 is ground\nT22 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="A: insert(0, T22, T32)\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: insert(0, T22, T32), SCOPE: 3, CLAUSE: 0 | insert(0, T22, T32), SCOPE: 3, CLAUSE: 1 | insert(0, T22, T32), SCOPE: 3, CLAUSE: 2 | insert(0, T22, T32), SCOPE: 3, CLAUSE: 3\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: insert(0, T22, T32), SCOPE: 3, CLAUSE: 0\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: insert(0, T22, T32), SCOPE: 3, CLAUSE: 1 | insert(0, T22, T32), SCOPE: 3, CLAUSE: 2 | insert(0, T22, T32), SCOPE: 3, CLAUSE: 3\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: insert(0, T22, T32), SCOPE: 3, CLAUSE: 1\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: insert(0, T22, T32), SCOPE: 3, CLAUSE: 2 | insert(0, T22, T32), SCOPE: 3, CLAUSE: 3\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: insert(0, T22, T32), SCOPE: 3, CLAUSE: 2\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: insert(0, T22, T32), SCOPE: 3, CLAUSE: 3\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(less(0, T59), insert(0, T60, T63))\n\nT59 is ground\nT60 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="B: less(0, T59)\n\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: insert(0, T60, T63)\n\nT60 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: less(0, T59), SCOPE: 4, CLAUSE: 4 | less(0, T59), SCOPE: 4, CLAUSE: 5\n\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: less(0, T59), SCOPE: 4, CLAUSE: 4\n\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: less(0, T59), SCOPE: 4, CLAUSE: 5\n\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(less(T81, 0), insert(0, T83, T85))\n\nT81 is ground\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="C: less(T81, 0)\n\nT81 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: insert(0, T83, T85)\n\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: less(T81, 0), SCOPE: 5, CLAUSE: 4 | less(T81, 0), SCOPE: 5, CLAUSE: 5\n\nT81 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: less(T81, 0), SCOPE: 5, CLAUSE: 5\n\nT81 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(less(T25, T21), insert(T25, T22, T26)), SCOPE: 2, CLAUSE: 5\n\nT21 is ground\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ?_2 | insert(T1, tree(T21, T22, T23), T3), SCOPE: 1, CLAUSE: 3\n\nT21 is ground\nT22 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="I: ','(less(T97, T96), insert(s(T97), T22, T98))\n\nT22 is ground\nT96 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="D: less(T97, T96)\n\nT96 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="E: insert(s(T101), T22, T102)\n\nT22 is ground\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: less(T97, T96), SCOPE: 6, CLAUSE: 4 | less(T97, T96), SCOPE: 6, CLAUSE: 5\n\nT96 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: less(T97, T96), SCOPE: 6, CLAUSE: 4\n\nT96 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: less(T97, T96), SCOPE: 6, CLAUSE: 5\n\nT96 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: less(T116, T115)\n\nT115 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: insert(s(T101), T22, T102), SCOPE: 7, CLAUSE: 0 | insert(s(T101), T22, T102), SCOPE: 7, CLAUSE: 1 | insert(s(T101), T22, T102), SCOPE: 7, CLAUSE: 2 | insert(s(T101), T22, T102), SCOPE: 7, CLAUSE: 3\n\nT22 is ground\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: insert(s(T101), T22, T102), SCOPE: 7, CLAUSE: 0\n\nT22 is ground\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: insert(s(T101), T22, T102), SCOPE: 7, CLAUSE: 1 | insert(s(T101), T22, T102), SCOPE: 7, CLAUSE: 2 | insert(s(T101), T22, T102), SCOPE: 7, CLAUSE: 3\n\nT22 is ground\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: insert(s(T101), T22, T102), SCOPE: 7, CLAUSE: 1\n\nT22 is ground\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: insert(s(T101), T22, T102), SCOPE: 7, CLAUSE: 2 | insert(s(T101), T22, T102), SCOPE: 7, CLAUSE: 3\n\nT22 is ground\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: insert(s(T101), T22, T102), SCOPE: 7, CLAUSE: 2\n\nT22 is ground\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: insert(s(T101), T22, T102), SCOPE: 7, CLAUSE: 3\n\nT22 is ground\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(less(s(T161), T162), insert(s(T161), T163, T166))\n\nT161 is ground\nT162 is ground\nT163 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="F: less(s(T161), T162)\n\nT161 is ground\nT162 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: insert(s(T161), T163, T166)\n\nT161 is ground\nT163 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: less(s(T161), T162), SCOPE: 8, CLAUSE: 4 | less(s(T161), T162), SCOPE: 8, CLAUSE: 5\n\nT161 is ground\nT162 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: less(s(T161), T162), SCOPE: 8, CLAUSE: 5\n\nT161 is ground\nT162 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="G: less(T171, T172)\n\nT171 is ground\nT172 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: less(T171, T172), SCOPE: 9, CLAUSE: 4 | less(T171, T172), SCOPE: 9, CLAUSE: 5\n\nT171 is ground\nT172 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: less(T171, T172), SCOPE: 9, CLAUSE: 4\n\nT171 is ground\nT172 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: less(T171, T172), SCOPE: 9, CLAUSE: 5\n\nT171 is ground\nT172 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: less(T184, T185)\n\nT184 is ground\nT185 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(less(T201, s(T200)), insert(s(T200), T203, T205))\n\nT200 is ground\nT201 is ground\nT203 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: less(T201, s(T200))\n\nT200 is ground\nT201 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: insert(s(T200), T203, T205)\n\nT200 is ground\nT203 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: insert(T1, tree(T21, T22, T23), T3), SCOPE: 1, CLAUSE: 3\n\nT21 is ground\nT22 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="J: ','(less(T223, T227), insert(T227, T225, T228))\n\nT223 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="K: less(T223, T227)\n\nT223 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: insert(T231, T225, T232)\n\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: less(T223, T227), SCOPE: 10, CLAUSE: 4 | less(T223, T227), SCOPE: 10, CLAUSE: 5\n\nT223 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: less(T223, T227), SCOPE: 10, CLAUSE: 4\n\nT223 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: less(T223, T227), SCOPE: 10, CLAUSE: 5\n\nT223 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: less(T244, T246)\n\nT244 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(less(T257, T261), insert(T261, T259, T262))\n\nT257 is ground\nT258 is ground\nT259 is ground\nX28 is free\nX29 is free\nX30 is free\nX31 is free\nX32 is free\ninsert(T1, tree(T257, T258, T259), T3) !=? insert(X28, tree(X29, X30, X31), tree(X29, X32, X31))", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(less(T257, T261), insert(T261, T259, T262)), SCOPE: 11, CLAUSE: 4 | ','(less(T257, T261), insert(T261, T259, T262)), SCOPE: 11, CLAUSE: 5\n\nT257 is ground\nT258 is ground\nT259 is ground\nX28 is free\nX29 is free\nX30 is free\nX31 is free\nX32 is free\ninsert(T1, tree(T257, T258, T259), T3) !=? insert(X28, tree(X29, X30, X31), tree(X29, X32, X31))", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(less(T257, T261), insert(T261, T259, T262)), SCOPE: 11, CLAUSE: 4\n\nT257 is ground\nT258 is ground\nT259 is ground\nX28 is free\nX29 is free\nX30 is free\nX31 is free\nX32 is free\ninsert(T1, tree(T257, T258, T259), T3) !=? insert(X28, tree(X29, X30, X31), tree(X29, X32, X31))", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(less(T257, T261), insert(T261, T259, T262)), SCOPE: 11, CLAUSE: 5\n\nT257 is ground\nT258 is ground\nT259 is ground\nX28 is free\nX29 is free\nX30 is free\nX31 is free\nX32 is free\ninsert(T1, tree(T257, T258, T259), T3) !=? insert(X28, tree(X29, X30, X31), tree(X29, X32, X31))", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: insert(s(T269), T259, T268)\n\nT258 is ground\nT259 is ground\nX28 is free\nX29 is free\nX30 is free\nX31 is free\nX32 is free\ninsert(T1, tree(0, T258, T259), T3) !=? insert(X28, tree(X29, X30, X31), tree(X29, X32, X31))", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(less(T276, T278), insert(s(T278), T259, T279))\n\nT258 is ground\nT259 is ground\nT276 is ground\nX28 is free\nX29 is free\nX30 is free\nX31 is free\nX32 is free\ninsert(T1, tree(s(T276), T258, T259), T3) !=? insert(X28, tree(X29, X30, X31), tree(X29, X32, X31))", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: less(T276, T278)\n\nT258 is ground\nT259 is ground\nT276 is ground\nX28 is free\nX29 is free\nX30 is free\nX31 is free\nX32 is free\ninsert(T1, tree(s(T276), T258, T259), T3) !=? insert(X28, tree(X29, X30, X31), tree(X29, X32, X31))", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: insert(s(T282), T259, T283)\n\nT258 is ground\nT259 is ground\nT276 is ground\nX28 is free\nX29 is free\nX30 is free\nX31 is free\nX32 is free\ninsert(T284, tree(s(T276), T258, T259), T285) !=? insert(X28, tree(X29, X30, X31), tree(X29, X32, X31))", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: ','(less(T300, T296), insert(T300, T297, T301)) | insert(T1, tree(T296, T297, T298), T3), SCOPE: 1, CLAUSE: 3\n\nT296 is ground\nT297 is ground\nT298 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(T296, T297, T298), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT2 is ground\nX3 is free\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, T2, T3) !=? insert(X3, void, tree(X3, void, void))\ninsert(T1, T2, T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(less(T300, T296), insert(T300, T297, T301)), SCOPE: 12, CLAUSE: 4 | ','(less(T300, T296), insert(T300, T297, T301)), SCOPE: 12, CLAUSE: 5 | ?_12 | insert(T1, tree(T296, T297, T298), T3), SCOPE: 1, CLAUSE: 3\n\nT296 is ground\nT297 is ground\nT298 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(T296, T297, T298), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(less(T300, T296), insert(T300, T297, T301)), SCOPE: 12, CLAUSE: 4\n\nT296 is ground\nT297 is ground\nT298 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(T296, T297, T298), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(less(T300, T296), insert(T300, T297, T301)), SCOPE: 12, CLAUSE: 5 | ?_12 | insert(T1, tree(T296, T297, T298), T3), SCOPE: 1, CLAUSE: 3\n\nT296 is ground\nT297 is ground\nT298 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(T296, T297, T298), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: insert(0, T297, T307)\n\nT297 is ground\nT298 is ground\nT306 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(s(T306), T297, T298), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ','(less(T300, T296), insert(T300, T297, T301)), SCOPE: 12, CLAUSE: 5\n\nT296 is ground\nT297 is ground\nT298 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(T296, T297, T298), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ?_12 | insert(T1, tree(T296, T297, T298), T3), SCOPE: 1, CLAUSE: 3\n\nT296 is ground\nT297 is ground\nT298 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(T296, T297, T298), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(less(T318, T317), insert(s(T318), T297, T319))\n\nT297 is ground\nT298 is ground\nT317 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(s(T317), T297, T298), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: insert(T1, tree(T296, T297, T298), T3), SCOPE: 1, CLAUSE: 3\n\nT296 is ground\nT297 is ground\nT298 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(T296, T297, T298), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ','(less(T333, T337), insert(T337, T335, T338))\n\nT333 is ground\nT334 is ground\nT335 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(T333, T334, T335), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ','(less(T347, T351), insert(T351, T349, T352))\n\nT347 is ground\nT348 is ground\nT349 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(T347, T348, T349), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(less(T347, T351), insert(T351, T349, T352)), SCOPE: 13, CLAUSE: 4 | ','(less(T347, T351), insert(T351, T349, T352)), SCOPE: 13, CLAUSE: 5\n\nT347 is ground\nT348 is ground\nT349 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(T347, T348, T349), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: ','(less(T347, T351), insert(T351, T349, T352)), SCOPE: 13, CLAUSE: 4\n\nT347 is ground\nT348 is ground\nT349 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(T347, T348, T349), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ','(less(T347, T351), insert(T351, T349, T352)), SCOPE: 13, CLAUSE: 5\n\nT347 is ground\nT348 is ground\nT349 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(T347, T348, T349), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: insert(s(T359), T349, T358)\n\nT348 is ground\nT349 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(0, T348, T349), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: ','(less(T366, T368), insert(s(T368), T349, T369))\n\nT348 is ground\nT349 is ground\nT366 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(s(T366), T348, T349), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: less(T366, T368)\n\nT348 is ground\nT349 is ground\nT366 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T1, tree(s(T366), T348, T349), T3) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: insert(s(T372), T349, T373)\n\nT348 is ground\nT349 is ground\nT366 is ground\nX20 is free\nX21 is free\nX22 is free\ninsert(T374, tree(s(T366), T348, T349), T375) !=? insert(X20, tree(X20, X21, X22), tree(X20, X21, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 146 [arrowhead = none ];
146 -> 2;

147 [label="EVAL with clause\ninsert(X3, void, tree(X3, void, void)).\nand substitutionT1 -> T5,\nX3 -> T5,\nT2 -> void,\nT3 -> tree(T5, void, void)", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 147 [arrowhead = none ];
147 -> 3;

148 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
2 -> 148 [arrowhead = none ];
148 -> 4;

149 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 149 [arrowhead = none ];
149 -> 5;

150 [label="EVAL with clause\ninsert(X20, tree(X20, X21, X22), tree(X20, X21, X22)).\nand substitutionT1 -> T12,\nX20 -> T12,\nX21 -> T13,\nX22 -> T14,\nT2 -> tree(T12, T13, T14),\nT3 -> tree(T12, T13, T14)", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 150 [arrowhead = none ];
150 -> 9;

151 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 151 [arrowhead = none ];
151 -> 10;

152 [label="BACKTRACK\nfor clause: insert(X, tree(X, Left, Right), tree(X, Left, Right))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 152 [arrowhead = none ];
152 -> 6;

153 [label="BACKTRACK\nfor clause: insert(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), insert(X, Left, Left1))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 153 [arrowhead = none ];
153 -> 7;

154 [label="BACKTRACK\nfor clause: insert(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), insert(X, Right, Right1))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 154 [arrowhead = none ];
154 -> 8;

155 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 155 [arrowhead = none ];
155 -> 11;

156 [label="EVAL with clause\ninsert(X313, tree(X314, X315, X316), tree(X314, X317, X316)) :- ','(less(X313, X314), insert(X313, X315, X317)).\nand substitutionT1 -> T300,\nX313 -> T300,\nX314 -> T296,\nX315 -> T297,\nX316 -> T298,\nT2 -> tree(T296, T297, T298),\nX317 -> T301,\nT3 -> tree(T296, T301, T298),\nT295 -> T300,\nT299 -> T301", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 156 [arrowhead = none ];
156 -> 121;

157 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 157 [arrowhead = none ];
157 -> 122;

158 [label="EVAL with clause\ninsert(X28, tree(X29, X30, X31), tree(X29, X32, X31)) :- ','(less(X28, X29), insert(X28, X30, X32)).\nand substitutionT1 -> T25,\nX28 -> T25,\nT12 -> T21,\nX29 -> T21,\nT13 -> T22,\nX30 -> T22,\nT14 -> T23,\nX31 -> T23,\nX32 -> T26,\nT3 -> tree(T21, T26, T23),\nT20 -> T25,\nT24 -> T26", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 158 [arrowhead = none ];
158 -> 12;

159 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 159 [arrowhead = none ];
159 -> 13;

160 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
12 -> 160 [arrowhead = none ];
160 -> 14;

161 [label="EVAL with clause\ninsert(X284, tree(X285, X286, X287), tree(X285, X286, X288)) :- ','(less(X285, X284), insert(X284, X287, X288)).\nand substitutionT1 -> T261,\nX284 -> T261,\nT12 -> T257,\nX285 -> T257,\nT13 -> T258,\nX286 -> T258,\nT14 -> T259,\nX287 -> T259,\nX288 -> T262,\nT3 -> tree(T257, T258, T262),\nT256 -> T261,\nT260 -> T262", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 161 [arrowhead = none ];
161 -> 110;

162 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 162 [arrowhead = none ];
162 -> 111;

163 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 163 [arrowhead = none ];
163 -> 15;

164 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 164 [arrowhead = none ];
164 -> 16;

165 [label="EVAL with clause\nless(0, s(X37)).\nand substitutionT25 -> 0,\nX37 -> T31,\nT21 -> s(T31),\nT26 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 165 [arrowhead = none ];
165 -> 17;

166 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 166 [arrowhead = none ];
166 -> 18;

167 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
16 -> 167 [arrowhead = none ];
167 -> 50;

168 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
16 -> 168 [arrowhead = none ];
168 -> 51;

169 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
17 -> 169 [arrowhead = none ];
169 -> 19;

170 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
19 -> 170 [arrowhead = none ];
170 -> 20;

171 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
19 -> 171 [arrowhead = none ];
171 -> 21;

172 [label="EVAL with clause\ninsert(X44, void, tree(X44, void, void)).\nand substitutionX44 -> 0,\nT22 -> void,\nT32 -> tree(0, void, void)", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 172 [arrowhead = none ];
172 -> 22;

173 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 173 [arrowhead = none ];
173 -> 23;

174 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
21 -> 174 [arrowhead = none ];
174 -> 25;

175 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
21 -> 175 [arrowhead = none ];
175 -> 26;

176 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 176 [arrowhead = none ];
176 -> 24;

177 [label="EVAL with clause\ninsert(X57, tree(X57, X58, X59), tree(X57, X58, X59)).\nand substitutionX57 -> 0,\nX58 -> T41,\nX59 -> T42,\nT22 -> tree(0, T41, T42),\nT32 -> tree(0, T41, T42)", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 177 [arrowhead = none ];
177 -> 27;

178 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 178 [arrowhead = none ];
178 -> 28;

179 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 179 [arrowhead = none ];
179 -> 30;

180 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 180 [arrowhead = none ];
180 -> 31;

181 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 181 [arrowhead = none ];
181 -> 29;

182 [label="EVAL with clause\ninsert(X80, tree(X81, X82, X83), tree(X81, X84, X83)) :- ','(less(X80, X81), insert(X80, X82, X84)).\nand substitutionX80 -> 0,\nX81 -> T59,\nX82 -> T60,\nX83 -> T61,\nT22 -> tree(T59, T60, T61),\nX84 -> T63,\nT32 -> tree(T59, T63, T61),\nT62 -> T63", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 182 [arrowhead = none ];
182 -> 32;

183 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 183 [arrowhead = none ];
183 -> 33;

184 [label="EVAL with clause\ninsert(X108, tree(X109, X110, X111), tree(X109, X110, X112)) :- ','(less(X109, X108), insert(X108, X111, X112)).\nand substitutionX108 -> 0,\nX109 -> T81,\nX110 -> T82,\nX111 -> T83,\nT22 -> tree(T81, T82, T83),\nX112 -> T85,\nT32 -> tree(T81, T82, T85),\nT84 -> T85", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 184 [arrowhead = none ];
184 -> 43;

185 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 185 [arrowhead = none ];
185 -> 44;

186 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
32 -> 186 [arrowhead = none ];
186 -> 34;

187 [label="SPLIT 2\nnew knowledge:\nT59 is ground", fontsize=14, style = filled, fillcolor = violet];
32 -> 187 [arrowhead = none ];
187 -> 35;

188 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
34 -> 188 [arrowhead = none ];
188 -> 36;

189 [label="INSTANCE with matching:\nT22 -> T60\nT32 -> T63", fontsize=14, style = filled, fillcolor = lightgrey];
35 -> 189 [arrowhead = none , style=dashed];
189 -> 17[style=dashed];

190 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 190 [arrowhead = none ];
190 -> 37;

191 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 191 [arrowhead = none ];
191 -> 38;

192 [label="EVAL with clause\nless(0, s(X93)).\nand substitutionX93 -> T72,\nT59 -> s(T72)", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 192 [arrowhead = none ];
192 -> 39;

193 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 193 [arrowhead = none ];
193 -> 40;

194 [label="BACKTRACK\nfor clause: less(s(X), s(Y)) :- less(X, Y)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
38 -> 194 [arrowhead = none ];
194 -> 42;

195 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 195 [arrowhead = none ];
195 -> 41;

196 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
43 -> 196 [arrowhead = none ];
196 -> 45;

197 [label="SPLIT 2\nnew knowledge:\nT81 is ground", fontsize=14, style = filled, fillcolor = violet];
43 -> 197 [arrowhead = none ];
197 -> 46;

198 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
45 -> 198 [arrowhead = none ];
198 -> 47;

199 [label="INSTANCE with matching:\nT22 -> T83\nT32 -> T85", fontsize=14, style = filled, fillcolor = lightgrey];
46 -> 199 [arrowhead = none , style=dashed];
199 -> 17[style=dashed];

200 [label="BACKTRACK\nfor clause: less(0, s(X1))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 200 [arrowhead = none ];
200 -> 48;

201 [label="BACKTRACK\nfor clause: less(s(X), s(Y)) :- less(X, Y)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 201 [arrowhead = none ];
201 -> 49;

202 [label="EVAL with clause\nless(s(X130), s(X131)) :- less(X130, X131).\nand substitutionX130 -> T97,\nT25 -> s(T97),\nX131 -> T96,\nT21 -> s(T96),\nT95 -> T97,\nT26 -> T98", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 202 [arrowhead = none ];
202 -> 52;

203 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
50 -> 203 [arrowhead = none ];
203 -> 53;

204 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 204 [arrowhead = none ];
204 -> 97;

205 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
52 -> 205 [arrowhead = none ];
205 -> 54;

206 [label="SPLIT 2\nnew knowledge:\nT101 is ground\nT96 is ground\nreplacements:T97 -> T101,\nT98 -> T102", fontsize=14, style = filled, fillcolor = violet];
52 -> 206 [arrowhead = none ];
206 -> 55;

207 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
54 -> 207 [arrowhead = none ];
207 -> 56;

208 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
55 -> 208 [arrowhead = none ];
208 -> 64;

209 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
56 -> 209 [arrowhead = none ];
209 -> 57;

210 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
56 -> 210 [arrowhead = none ];
210 -> 58;

211 [label="EVAL with clause\nless(0, s(X140)).\nand substitutionT97 -> 0,\nX140 -> T109,\nT96 -> s(T109)", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 211 [arrowhead = none ];
211 -> 59;

212 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 212 [arrowhead = none ];
212 -> 60;

213 [label="EVAL with clause\nless(s(X145), s(X146)) :- less(X145, X146).\nand substitutionX145 -> T116,\nT97 -> s(T116),\nX146 -> T115,\nT96 -> s(T115),\nT114 -> T116", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 213 [arrowhead = none ];
213 -> 62;

214 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
58 -> 214 [arrowhead = none ];
214 -> 63;

215 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 215 [arrowhead = none ];
215 -> 61;

216 [label="INSTANCE with matching:\nT97 -> T116\nT96 -> T115", fontsize=14, style = filled, fillcolor = lightgrey];
62 -> 216 [arrowhead = none , style=dashed];
216 -> 54[style=dashed];

217 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
64 -> 217 [arrowhead = none ];
217 -> 65;

218 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
64 -> 218 [arrowhead = none ];
218 -> 66;

219 [label="EVAL with clause\ninsert(X155, void, tree(X155, void, void)).\nand substitutionT101 -> T125,\nX155 -> s(T125),\nT22 -> void,\nT102 -> tree(s(T125), void, void)", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 219 [arrowhead = none ];
219 -> 67;

220 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 220 [arrowhead = none ];
220 -> 68;

221 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 221 [arrowhead = none ];
221 -> 70;

222 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 222 [arrowhead = none ];
222 -> 71;

223 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
67 -> 223 [arrowhead = none ];
223 -> 69;

224 [label="EVAL with clause\ninsert(X168, tree(X168, X169, X170), tree(X168, X169, X170)).\nand substitutionT101 -> T138,\nX168 -> s(T138),\nX169 -> T139,\nX170 -> T140,\nT22 -> tree(s(T138), T139, T140),\nT102 -> tree(s(T138), T139, T140)", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 224 [arrowhead = none ];
224 -> 72;

225 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
70 -> 225 [arrowhead = none ];
225 -> 73;

226 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
71 -> 226 [arrowhead = none ];
226 -> 75;

227 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
71 -> 227 [arrowhead = none ];
227 -> 76;

228 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 228 [arrowhead = none ];
228 -> 74;

229 [label="EVAL with clause\ninsert(X191, tree(X192, X193, X194), tree(X192, X195, X194)) :- ','(less(X191, X192), insert(X191, X193, X195)).\nand substitutionT101 -> T161,\nX191 -> s(T161),\nX192 -> T162,\nX193 -> T163,\nX194 -> T164,\nT22 -> tree(T162, T163, T164),\nX195 -> T166,\nT102 -> tree(T162, T166, T164),\nT165 -> T166", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 229 [arrowhead = none ];
229 -> 77;

230 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
75 -> 230 [arrowhead = none ];
230 -> 78;

231 [label="EVAL with clause\ninsert(X234, tree(X235, X236, X237), tree(X235, X236, X238)) :- ','(less(X235, X234), insert(X234, X237, X238)).\nand substitutionT101 -> T200,\nX234 -> s(T200),\nX235 -> T201,\nX236 -> T202,\nX237 -> T203,\nT22 -> tree(T201, T202, T203),\nX238 -> T205,\nT102 -> tree(T201, T202, T205),\nT204 -> T205", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 231 [arrowhead = none ];
231 -> 93;

232 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 232 [arrowhead = none ];
232 -> 94;

233 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
77 -> 233 [arrowhead = none ];
233 -> 79;

234 [label="SPLIT 2\nnew knowledge:\nT161 is ground\nT162 is ground", fontsize=14, style = filled, fillcolor = violet];
77 -> 234 [arrowhead = none ];
234 -> 80;

235 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
79 -> 235 [arrowhead = none ];
235 -> 81;

236 [label="INSTANCE with matching:\nT101 -> T161\nT22 -> T163\nT102 -> T166", fontsize=14, style = filled, fillcolor = lightgrey];
80 -> 236 [arrowhead = none , style=dashed];
236 -> 55[style=dashed];

237 [label="BACKTRACK\nfor clause: less(0, s(X1))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
81 -> 237 [arrowhead = none ];
237 -> 82;

238 [label="EVAL with clause\nless(s(X205), s(X206)) :- less(X205, X206).\nand substitutionT161 -> T171,\nX205 -> T171,\nX206 -> T172,\nT162 -> s(T172)", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 238 [arrowhead = none ];
238 -> 83;

239 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 239 [arrowhead = none ];
239 -> 84;

240 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
83 -> 240 [arrowhead = none ];
240 -> 85;

241 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
85 -> 241 [arrowhead = none ];
241 -> 86;

242 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
85 -> 242 [arrowhead = none ];
242 -> 87;

243 [label="EVAL with clause\nless(0, s(X213)).\nand substitutionT171 -> 0,\nX213 -> T179,\nT172 -> s(T179)", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 243 [arrowhead = none ];
243 -> 88;

244 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
86 -> 244 [arrowhead = none ];
244 -> 89;

245 [label="EVAL with clause\nless(s(X218), s(X219)) :- less(X218, X219).\nand substitutionX218 -> T184,\nT171 -> s(T184),\nX219 -> T185,\nT172 -> s(T185)", fontsize=14, style = filled, fillcolor = lightblue];
87 -> 245 [arrowhead = none ];
245 -> 91;

246 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
87 -> 246 [arrowhead = none ];
246 -> 92;

247 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 247 [arrowhead = none ];
247 -> 90;

248 [label="INSTANCE with matching:\nT171 -> T184\nT172 -> T185", fontsize=14, style = filled, fillcolor = lightgrey];
91 -> 248 [arrowhead = none , style=dashed];
248 -> 83[style=dashed];

249 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
93 -> 249 [arrowhead = none ];
249 -> 95;

250 [label="SPLIT 2\nnew knowledge:\nT201 is ground\nT200 is ground", fontsize=14, style = filled, fillcolor = violet];
93 -> 250 [arrowhead = none ];
250 -> 96;

251 [label="INSTANCE with matching:\nT171 -> T201\nT172 -> s(T200)", fontsize=14, style = filled, fillcolor = lightgrey];
95 -> 251 [arrowhead = none , style=dashed];
251 -> 83[style=dashed];

252 [label="INSTANCE with matching:\nT101 -> T200\nT22 -> T203\nT102 -> T205", fontsize=14, style = filled, fillcolor = lightgrey];
96 -> 252 [arrowhead = none , style=dashed];
252 -> 55[style=dashed];

253 [label="EVAL with clause\ninsert(X255, tree(X256, X257, X258), tree(X256, X257, X259)) :- ','(less(X256, X255), insert(X255, X258, X259)).\nand substitutionT1 -> T227,\nX255 -> T227,\nT21 -> T223,\nX256 -> T223,\nT22 -> T224,\nX257 -> T224,\nT23 -> T225,\nX258 -> T225,\nX259 -> T228,\nT3 -> tree(T223, T224, T228),\nT222 -> T227,\nT226 -> T228", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 253 [arrowhead = none ];
253 -> 98;

254 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
97 -> 254 [arrowhead = none ];
254 -> 99;

255 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
98 -> 255 [arrowhead = none ];
255 -> 100;

256 [label="SPLIT 2\nnew knowledge:\nT223 is ground\nreplacements:T227 -> T231,\nT228 -> T232", fontsize=14, style = filled, fillcolor = violet];
98 -> 256 [arrowhead = none ];
256 -> 101;

257 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
100 -> 257 [arrowhead = none ];
257 -> 102;

258 [label="INSTANCE with matching:\nT1 -> T231\nT2 -> T225\nT3 -> T232", fontsize=14, style = filled, fillcolor = lightgrey];
101 -> 258 [arrowhead = none , style=dashed];
258 -> 1[style=dashed];

259 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
102 -> 259 [arrowhead = none ];
259 -> 103;

260 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
102 -> 260 [arrowhead = none ];
260 -> 104;

261 [label="EVAL with clause\nless(0, s(X268)).\nand substitutionT223 -> 0,\nX268 -> T239,\nT227 -> s(T239)", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 261 [arrowhead = none ];
261 -> 105;

262 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
103 -> 262 [arrowhead = none ];
262 -> 106;

263 [label="EVAL with clause\nless(s(X273), s(X274)) :- less(X273, X274).\nand substitutionX273 -> T244,\nT223 -> s(T244),\nX274 -> T246,\nT227 -> s(T246),\nT245 -> T246", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 263 [arrowhead = none ];
263 -> 108;

264 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
104 -> 264 [arrowhead = none ];
264 -> 109;

265 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
105 -> 265 [arrowhead = none ];
265 -> 107;

266 [label="INSTANCE with matching:\nT223 -> T244\nT227 -> T246", fontsize=14, style = filled, fillcolor = lightgrey];
108 -> 266 [arrowhead = none , style=dashed];
266 -> 100[style=dashed];

267 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
110 -> 267 [arrowhead = none ];
267 -> 112;

268 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
112 -> 268 [arrowhead = none ];
268 -> 113;

269 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
112 -> 269 [arrowhead = none ];
269 -> 114;

270 [label="EVAL with clause\nless(0, s(X293)).\nand substitutionT257 -> 0,\nX293 -> T269,\nT261 -> s(T269),\nT262 -> T268,\nT267 -> T269", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 270 [arrowhead = none ];
270 -> 115;

271 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
113 -> 271 [arrowhead = none ];
271 -> 116;

272 [label="EVAL with clause\nless(s(X300), s(X301)) :- less(X300, X301).\nand substitutionX300 -> T276,\nT257 -> s(T276),\nX301 -> T278,\nT261 -> s(T278),\nT277 -> T278,\nT262 -> T279", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 272 [arrowhead = none ];
272 -> 117;

273 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
114 -> 273 [arrowhead = none ];
273 -> 118;

274 [label="INSTANCE with matching:\nT1 -> s(T269)\nT2 -> T259\nT3 -> T268", fontsize=14, style = filled, fillcolor = lightgrey];
115 -> 274 [arrowhead = none , style=dashed];
274 -> 1[style=dashed];

275 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
117 -> 275 [arrowhead = none ];
275 -> 119;

276 [label="SPLIT 2\nnew knowledge:\nT276 is ground\nreplacements:T278 -> T282,\nT279 -> T283,\nT1 -> T284,\nT3 -> T285", fontsize=14, style = filled, fillcolor = violet];
117 -> 276 [arrowhead = none ];
276 -> 120;

277 [label="INSTANCE with matching:\nT223 -> T276\nT227 -> T278", fontsize=14, style = filled, fillcolor = lightgrey];
119 -> 277 [arrowhead = none , style=dashed];
277 -> 100[style=dashed];

278 [label="INSTANCE with matching:\nT1 -> s(T282)\nT2 -> T259\nT3 -> T283", fontsize=14, style = filled, fillcolor = lightgrey];
120 -> 278 [arrowhead = none , style=dashed];
278 -> 1[style=dashed];

279 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
121 -> 279 [arrowhead = none ];
279 -> 123;

280 [label="EVAL with clause\ninsert(X359, tree(X360, X361, X362), tree(X360, X361, X363)) :- ','(less(X360, X359), insert(X359, X362, X363)).\nand substitutionT1 -> T351,\nX359 -> T351,\nX360 -> T347,\nX361 -> T348,\nX362 -> T349,\nT2 -> tree(T347, T348, T349),\nX363 -> T352,\nT3 -> tree(T347, T348, T352),\nT346 -> T351,\nT350 -> T352", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 280 [arrowhead = none ];
280 -> 135;

281 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
122 -> 281 [arrowhead = none ];
281 -> 136;

282 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
123 -> 282 [arrowhead = none ];
282 -> 124;

283 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
123 -> 283 [arrowhead = none ];
283 -> 125;

284 [label="EVAL with clause\nless(0, s(X322)).\nand substitutionT300 -> 0,\nX322 -> T306,\nT296 -> s(T306),\nT301 -> T307", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 284 [arrowhead = none ];
284 -> 126;

285 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
124 -> 285 [arrowhead = none ];
285 -> 127;

286 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
125 -> 286 [arrowhead = none ];
286 -> 128;

287 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
125 -> 287 [arrowhead = none ];
287 -> 129;

288 [label="INSTANCE with matching:\nT22 -> T297\nT32 -> T307", fontsize=14, style = filled, fillcolor = lightgrey];
126 -> 288 [arrowhead = none , style=dashed];
288 -> 17[style=dashed];

289 [label="EVAL with clause\nless(s(X333), s(X334)) :- less(X333, X334).\nand substitutionX333 -> T318,\nT300 -> s(T318),\nX334 -> T317,\nT296 -> s(T317),\nT316 -> T318,\nT301 -> T319", fontsize=14, style = filled, fillcolor = lightblue];
128 -> 289 [arrowhead = none ];
289 -> 130;

290 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
128 -> 290 [arrowhead = none ];
290 -> 131;

291 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
129 -> 291 [arrowhead = none ];
291 -> 132;

292 [label="INSTANCE with matching:\nT97 -> T318\nT96 -> T317\nT22 -> T297\nT98 -> T319", fontsize=14, style = filled, fillcolor = lightgrey];
130 -> 292 [arrowhead = none , style=dashed];
292 -> 52[style=dashed];

293 [label="EVAL with clause\ninsert(X347, tree(X348, X349, X350), tree(X348, X349, X351)) :- ','(less(X348, X347), insert(X347, X350, X351)).\nand substitutionT1 -> T337,\nX347 -> T337,\nT296 -> T333,\nX348 -> T333,\nT297 -> T334,\nX349 -> T334,\nT298 -> T335,\nX350 -> T335,\nX351 -> T338,\nT3 -> tree(T333, T334, T338),\nT332 -> T337,\nT336 -> T338", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 293 [arrowhead = none ];
293 -> 133;

294 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
132 -> 294 [arrowhead = none ];
294 -> 134;

295 [label="INSTANCE with matching:\nT223 -> T333\nT227 -> T337\nT225 -> T335\nT228 -> T338", fontsize=14, style = filled, fillcolor = lightgrey];
133 -> 295 [arrowhead = none , style=dashed];
295 -> 98[style=dashed];

296 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
135 -> 296 [arrowhead = none ];
296 -> 137;

297 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
137 -> 297 [arrowhead = none ];
297 -> 138;

298 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
137 -> 298 [arrowhead = none ];
298 -> 139;

299 [label="EVAL with clause\nless(0, s(X368)).\nand substitutionT347 -> 0,\nX368 -> T359,\nT351 -> s(T359),\nT352 -> T358,\nT357 -> T359", fontsize=14, style = filled, fillcolor = lightblue];
138 -> 299 [arrowhead = none ];
299 -> 140;

300 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
138 -> 300 [arrowhead = none ];
300 -> 141;

301 [label="EVAL with clause\nless(s(X375), s(X376)) :- less(X375, X376).\nand substitutionX375 -> T366,\nT347 -> s(T366),\nX376 -> T368,\nT351 -> s(T368),\nT367 -> T368,\nT352 -> T369", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 301 [arrowhead = none ];
301 -> 142;

302 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 302 [arrowhead = none ];
302 -> 143;

303 [label="INSTANCE with matching:\nT1 -> s(T359)\nT2 -> T349\nT3 -> T358", fontsize=14, style = filled, fillcolor = lightgrey];
140 -> 303 [arrowhead = none , style=dashed];
303 -> 1[style=dashed];

304 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
142 -> 304 [arrowhead = none ];
304 -> 144;

305 [label="SPLIT 2\nnew knowledge:\nT366 is ground\nreplacements:T368 -> T372,\nT369 -> T373,\nT1 -> T374,\nT3 -> T375", fontsize=14, style = filled, fillcolor = violet];
142 -> 305 [arrowhead = none ];
305 -> 145;

306 [label="INSTANCE with matching:\nT223 -> T366\nT227 -> T368", fontsize=14, style = filled, fillcolor = lightgrey];
144 -> 306 [arrowhead = none , style=dashed];
306 -> 100[style=dashed];

307 [label="INSTANCE with matching:\nT1 -> s(T372)\nT2 -> T349\nT3 -> T373", fontsize=14, style = filled, fillcolor = lightgrey];
145 -> 307 [arrowhead = none , style=dashed];
307 -> 1[style=dashed];

}

(2) Obligation:

Triples:

insertA(tree(X1, X2, X3), tree(X1, X4, X3)) :- ','(lesscB(X1), insertA(X2, X4)).
insertA(tree(X1, X2, X3), tree(X1, X2, X4)) :- ','(lesscC(X1), insertA(X3, X4)).
lessD(s(X1), s(X2)) :- lessD(X1, X2).
insertE(X1, tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- lessG(X1, X2).
insertE(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- ','(lesscF(X1, X2), insertE(X1, X3, X5)).
insertE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- lessG(X2, s(X1)).
insertE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- ','(lesscG(X2, s(X1)), insertE(X1, X4, X5)).
lessG(s(X1), s(X2)) :- lessG(X1, X2).
lessK(s(X1), s(X2)) :- lessK(X1, X2).
pI(X1, X2, X3, X4) :- lessD(X1, X2).
pI(X1, X2, X3, X4) :- ','(lesscD(X1, X2), insertE(X1, X3, X4)).
pJ(X1, X2, X3, X4) :- lessK(X1, X2).
pJ(X1, X2, X3, X4) :- ','(lesscK(X1, X2), insertH(X2, X3, X4)).
insertH(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- insertA(X2, X4).
insertH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- pI(X1, X2, X3, X5).
insertH(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pJ(X2, X1, X4, X5).
insertH(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- insertH(s(X1), X3, X4).
insertH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- lessK(X2, X1).
insertH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscK(X2, X1), insertH(s(X1), X4, X5)).
insertH(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- insertA(X2, X4).
insertH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- pI(X1, X2, X3, X5).
insertH(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pJ(X2, X1, X4, X5).
insertH(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- insertH(s(X1), X3, X4).
insertH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- lessK(X2, X1).
insertH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscK(X2, X1), insertH(s(X1), X4, X5)).

Clauses:

insertcA(void, tree(0, void, void)).
insertcA(tree(0, X1, X2), tree(0, X1, X2)).
insertcA(tree(X1, X2, X3), tree(X1, X4, X3)) :- ','(lesscB(X1), insertcA(X2, X4)).
insertcA(tree(X1, X2, X3), tree(X1, X2, X4)) :- ','(lesscC(X1), insertcA(X3, X4)).
lesscD(0, s(X1)).
lesscD(s(X1), s(X2)) :- lesscD(X1, X2).
insertcE(X1, void, tree(s(X1), void, void)).
insertcE(X1, tree(s(X1), X2, X3), tree(s(X1), X2, X3)).
insertcE(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- ','(lesscF(X1, X2), insertcE(X1, X3, X5)).
insertcE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- ','(lesscG(X2, s(X1)), insertcE(X1, X4, X5)).
lesscG(0, s(X1)).
lesscG(s(X1), s(X2)) :- lesscG(X1, X2).
insertcH(X1, void, tree(X1, void, void)).
insertcH(X1, tree(X1, X2, X3), tree(X1, X2, X3)).
insertcH(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- insertcA(X2, X4).
insertcH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- qcI(X1, X2, X3, X5).
insertcH(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcJ(X2, X1, X4, X5).
insertcH(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- insertcH(s(X1), X3, X4).
insertcH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscK(X2, X1), insertcH(s(X1), X4, X5)).
insertcH(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- insertcA(X2, X4).
insertcH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- qcI(X1, X2, X3, X5).
insertcH(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcJ(X2, X1, X4, X5).
insertcH(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- insertcH(s(X1), X3, X4).
insertcH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscK(X2, X1), insertcH(s(X1), X4, X5)).
lesscK(0, s(X1)).
lesscK(s(X1), s(X2)) :- lesscK(X1, X2).
qcI(X1, X2, X3, X4) :- ','(lesscD(X1, X2), insertcE(X1, X3, X4)).
qcJ(X1, X2, X3, X4) :- ','(lesscK(X1, X2), insertcH(X2, X3, X4)).
lesscB(s(X1)).
lesscF(X1, s(X2)) :- lesscG(X1, X2).

Afs:

insertH(x1, x2, x3)  =  insertH(x2)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [DT09].

(4) Obligation:

Triples:

insertA(tree(X1, X2, X3), tree(X1, X4, X3)) :- ','(lesscB(X1), insertA(X2, X4)).
lessD(s(X1), s(X2)) :- lessD(X1, X2).
insertE(X1, tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- lessG(X1, X2).
insertE(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- ','(lesscF(X1, X2), insertE(X1, X3, X5)).
insertE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- lessG(X2, s(X1)).
insertE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- ','(lesscG(X2, s(X1)), insertE(X1, X4, X5)).
lessG(s(X1), s(X2)) :- lessG(X1, X2).
lessK(s(X1), s(X2)) :- lessK(X1, X2).
pI(X1, X2, X3, X4) :- lessD(X1, X2).
pI(X1, X2, X3, X4) :- ','(lesscD(X1, X2), insertE(X1, X3, X4)).
pJ(X1, X2, X3, X4) :- lessK(X1, X2).
pJ(X1, X2, X3, X4) :- ','(lesscK(X1, X2), insertH(X2, X3, X4)).
insertH(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- insertA(X2, X4).
insertH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- pI(X1, X2, X3, X5).
insertH(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pJ(X2, X1, X4, X5).
insertH(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- insertH(s(X1), X3, X4).
insertH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- lessK(X2, X1).
insertH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscK(X2, X1), insertH(s(X1), X4, X5)).
insertH(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- insertA(X2, X4).
insertH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- pI(X1, X2, X3, X5).
insertH(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pJ(X2, X1, X4, X5).
insertH(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- insertH(s(X1), X3, X4).
insertH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- lessK(X2, X1).
insertH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscK(X2, X1), insertH(s(X1), X4, X5)).

Clauses:

insertcA(void, tree(0, void, void)).
insertcA(tree(0, X1, X2), tree(0, X1, X2)).
insertcA(tree(X1, X2, X3), tree(X1, X4, X3)) :- ','(lesscB(X1), insertcA(X2, X4)).
lesscD(0, s(X1)).
lesscD(s(X1), s(X2)) :- lesscD(X1, X2).
insertcE(X1, void, tree(s(X1), void, void)).
insertcE(X1, tree(s(X1), X2, X3), tree(s(X1), X2, X3)).
insertcE(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- ','(lesscF(X1, X2), insertcE(X1, X3, X5)).
insertcE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- ','(lesscG(X2, s(X1)), insertcE(X1, X4, X5)).
lesscG(0, s(X1)).
lesscG(s(X1), s(X2)) :- lesscG(X1, X2).
insertcH(X1, void, tree(X1, void, void)).
insertcH(X1, tree(X1, X2, X3), tree(X1, X2, X3)).
insertcH(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- insertcA(X2, X4).
insertcH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- qcI(X1, X2, X3, X5).
insertcH(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcJ(X2, X1, X4, X5).
insertcH(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- insertcH(s(X1), X3, X4).
insertcH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscK(X2, X1), insertcH(s(X1), X4, X5)).
insertcH(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- insertcA(X2, X4).
insertcH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- qcI(X1, X2, X3, X5).
insertcH(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcJ(X2, X1, X4, X5).
insertcH(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- insertcH(s(X1), X3, X4).
insertcH(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscK(X2, X1), insertcH(s(X1), X4, X5)).
lesscK(0, s(X1)).
lesscK(s(X1), s(X2)) :- lesscK(X1, X2).
qcI(X1, X2, X3, X4) :- ','(lesscD(X1, X2), insertcE(X1, X3, X4)).
qcJ(X1, X2, X3, X4) :- ','(lesscK(X1, X2), insertcH(X2, X3, X4)).
lesscB(s(X1)).
lesscF(X1, s(X2)) :- lesscG(X1, X2).

Afs:

insertH(x1, x2, x3)  =  insertH(x2)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
insertH_in: (f,b,f)
insertA_in: (b,f)
pI_in: (f,b,b,f)
lessD_in: (f,b)
lesscD_in: (f,b)
insertE_in: (b,b,f)
lessG_in: (b,b)
lesscF_in: (b,b)
lesscG_in: (b,b)
pJ_in: (b,f,b,f)
lessK_in: (b,f)
lesscK_in: (b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

INSERTH_IN_AGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U18_AGA(X1, X2, X3, X4, insertA_in_ga(X2, X4))
INSERTH_IN_AGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → INSERTA_IN_GA(X2, X4)
INSERTA_IN_GA(tree(X1, X2, X3), tree(X1, X4, X3)) → U1_GA(X1, X2, X3, X4, lesscB_in_g(X1))
U1_GA(X1, X2, X3, X4, lesscB_out_g(X1)) → U2_GA(X1, X2, X3, X4, insertA_in_ga(X2, X4))
U1_GA(X1, X2, X3, X4, lesscB_out_g(X1)) → INSERTA_IN_GA(X2, X4)
INSERTH_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U19_AGA(X1, X2, X3, X4, X5, pI_in_agga(X1, X2, X3, X5))
INSERTH_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → PI_IN_AGGA(X1, X2, X3, X5)
PI_IN_AGGA(X1, X2, X3, X4) → U12_AGGA(X1, X2, X3, X4, lessD_in_ag(X1, X2))
PI_IN_AGGA(X1, X2, X3, X4) → LESSD_IN_AG(X1, X2)
LESSD_IN_AG(s(X1), s(X2)) → U3_AG(X1, X2, lessD_in_ag(X1, X2))
LESSD_IN_AG(s(X1), s(X2)) → LESSD_IN_AG(X1, X2)
PI_IN_AGGA(X1, X2, X3, X4) → U13_AGGA(X1, X2, X3, X4, lesscD_in_ag(X1, X2))
U13_AGGA(X1, X2, X3, X4, lesscD_out_ag(X1, X2)) → U14_AGGA(X1, X2, X3, X4, insertE_in_gga(X1, X3, X4))
U13_AGGA(X1, X2, X3, X4, lesscD_out_ag(X1, X2)) → INSERTE_IN_GGA(X1, X3, X4)
INSERTE_IN_GGA(X1, tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U4_GGA(X1, X2, X3, X4, X5, lessG_in_gg(X1, X2))
INSERTE_IN_GGA(X1, tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → LESSG_IN_GG(X1, X2)
LESSG_IN_GG(s(X1), s(X2)) → U10_GG(X1, X2, lessG_in_gg(X1, X2))
LESSG_IN_GG(s(X1), s(X2)) → LESSG_IN_GG(X1, X2)
INSERTE_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U5_GGA(X1, X2, X3, X4, X5, lesscF_in_gg(X1, X2))
U5_GGA(X1, X2, X3, X4, X5, lesscF_out_gg(X1, X2)) → U6_GGA(X1, X2, X3, X4, X5, insertE_in_gga(X1, X3, X5))
U5_GGA(X1, X2, X3, X4, X5, lesscF_out_gg(X1, X2)) → INSERTE_IN_GGA(X1, X3, X5)
INSERTE_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U7_GGA(X1, X2, X3, X4, X5, lessG_in_gg(X2, s(X1)))
INSERTE_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → LESSG_IN_GG(X2, s(X1))
INSERTE_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U8_GGA(X1, X2, X3, X4, X5, lesscG_in_gg(X2, s(X1)))
U8_GGA(X1, X2, X3, X4, X5, lesscG_out_gg(X2, s(X1))) → U9_GGA(X1, X2, X3, X4, X5, insertE_in_gga(X1, X4, X5))
U8_GGA(X1, X2, X3, X4, X5, lesscG_out_gg(X2, s(X1))) → INSERTE_IN_GGA(X1, X4, X5)
INSERTH_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U20_AGA(X1, X2, X3, X4, X5, pJ_in_gaga(X2, X1, X4, X5))
INSERTH_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PJ_IN_GAGA(X2, X1, X4, X5)
PJ_IN_GAGA(X1, X2, X3, X4) → U15_GAGA(X1, X2, X3, X4, lessK_in_ga(X1, X2))
PJ_IN_GAGA(X1, X2, X3, X4) → LESSK_IN_GA(X1, X2)
LESSK_IN_GA(s(X1), s(X2)) → U11_GA(X1, X2, lessK_in_ga(X1, X2))
LESSK_IN_GA(s(X1), s(X2)) → LESSK_IN_GA(X1, X2)
PJ_IN_GAGA(X1, X2, X3, X4) → U16_GAGA(X1, X2, X3, X4, lesscK_in_ga(X1, X2))
U16_GAGA(X1, X2, X3, X4, lesscK_out_ga(X1, X2)) → U17_GAGA(X1, X2, X3, X4, insertH_in_aga(X2, X3, X4))
U16_GAGA(X1, X2, X3, X4, lesscK_out_ga(X1, X2)) → INSERTH_IN_AGA(X2, X3, X4)
INSERTH_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → U21_AGA(X1, X2, X3, X4, insertH_in_aga(s(X1), X3, X4))
INSERTH_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → INSERTH_IN_AGA(s(X1), X3, X4)
INSERTH_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U22_AGA(X1, X2, X3, X4, X5, lessK_in_ga(X2, X1))
INSERTH_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → LESSK_IN_GA(X2, X1)
INSERTH_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U23_AGA(X1, X2, X3, X4, X5, lesscK_in_ga(X2, X1))
U23_AGA(X1, X2, X3, X4, X5, lesscK_out_ga(X2, X1)) → U24_AGA(X1, X2, X3, X4, X5, insertH_in_aga(s(X1), X4, X5))
U23_AGA(X1, X2, X3, X4, X5, lesscK_out_ga(X2, X1)) → INSERTH_IN_AGA(s(X1), X4, X5)

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))
lesscD_in_ag(0, s(X1)) → lesscD_out_ag(0, s(X1))
lesscD_in_ag(s(X1), s(X2)) → U28_ag(X1, X2, lesscD_in_ag(X1, X2))
U28_ag(X1, X2, lesscD_out_ag(X1, X2)) → lesscD_out_ag(s(X1), s(X2))
lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
insertH_in_aga(x1, x2, x3)  =  insertH_in_aga(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
insertA_in_ga(x1, x2)  =  insertA_in_ga(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
pI_in_agga(x1, x2, x3, x4)  =  pI_in_agga(x2, x3)
lessD_in_ag(x1, x2)  =  lessD_in_ag(x2)
lesscD_in_ag(x1, x2)  =  lesscD_in_ag(x2)
lesscD_out_ag(x1, x2)  =  lesscD_out_ag(x1, x2)
U28_ag(x1, x2, x3)  =  U28_ag(x2, x3)
insertE_in_gga(x1, x2, x3)  =  insertE_in_gga(x1, x2)
lessG_in_gg(x1, x2)  =  lessG_in_gg(x1, x2)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
pJ_in_gaga(x1, x2, x3, x4)  =  pJ_in_gaga(x1, x3)
lessK_in_ga(x1, x2)  =  lessK_in_ga(x1)
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
INSERTH_IN_AGA(x1, x2, x3)  =  INSERTH_IN_AGA(x2)
U18_AGA(x1, x2, x3, x4, x5)  =  U18_AGA(x1, x2, x3, x5)
INSERTA_IN_GA(x1, x2)  =  INSERTA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)
U2_GA(x1, x2, x3, x4, x5)  =  U2_GA(x1, x2, x3, x5)
U19_AGA(x1, x2, x3, x4, x5, x6)  =  U19_AGA(x2, x3, x4, x6)
PI_IN_AGGA(x1, x2, x3, x4)  =  PI_IN_AGGA(x2, x3)
U12_AGGA(x1, x2, x3, x4, x5)  =  U12_AGGA(x2, x3, x5)
LESSD_IN_AG(x1, x2)  =  LESSD_IN_AG(x2)
U3_AG(x1, x2, x3)  =  U3_AG(x2, x3)
U13_AGGA(x1, x2, x3, x4, x5)  =  U13_AGGA(x2, x3, x5)
U14_AGGA(x1, x2, x3, x4, x5)  =  U14_AGGA(x1, x2, x3, x5)
INSERTE_IN_GGA(x1, x2, x3)  =  INSERTE_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4, x5, x6)  =  U4_GGA(x1, x2, x3, x4, x6)
LESSG_IN_GG(x1, x2)  =  LESSG_IN_GG(x1, x2)
U10_GG(x1, x2, x3)  =  U10_GG(x1, x2, x3)
U5_GGA(x1, x2, x3, x4, x5, x6)  =  U5_GGA(x1, x2, x3, x4, x6)
U6_GGA(x1, x2, x3, x4, x5, x6)  =  U6_GGA(x1, x2, x3, x4, x6)
U7_GGA(x1, x2, x3, x4, x5, x6)  =  U7_GGA(x1, x2, x3, x4, x6)
U8_GGA(x1, x2, x3, x4, x5, x6)  =  U8_GGA(x1, x2, x3, x4, x6)
U9_GGA(x1, x2, x3, x4, x5, x6)  =  U9_GGA(x1, x2, x3, x4, x6)
U20_AGA(x1, x2, x3, x4, x5, x6)  =  U20_AGA(x2, x3, x4, x6)
PJ_IN_GAGA(x1, x2, x3, x4)  =  PJ_IN_GAGA(x1, x3)
U15_GAGA(x1, x2, x3, x4, x5)  =  U15_GAGA(x1, x3, x5)
LESSK_IN_GA(x1, x2)  =  LESSK_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
U16_GAGA(x1, x2, x3, x4, x5)  =  U16_GAGA(x1, x3, x5)
U17_GAGA(x1, x2, x3, x4, x5)  =  U17_GAGA(x1, x3, x5)
U21_AGA(x1, x2, x3, x4, x5)  =  U21_AGA(x2, x3, x5)
U22_AGA(x1, x2, x3, x4, x5, x6)  =  U22_AGA(x2, x3, x4, x6)
U23_AGA(x1, x2, x3, x4, x5, x6)  =  U23_AGA(x2, x3, x4, x6)
U24_AGA(x1, x2, x3, x4, x5, x6)  =  U24_AGA(x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

INSERTH_IN_AGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U18_AGA(X1, X2, X3, X4, insertA_in_ga(X2, X4))
INSERTH_IN_AGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → INSERTA_IN_GA(X2, X4)
INSERTA_IN_GA(tree(X1, X2, X3), tree(X1, X4, X3)) → U1_GA(X1, X2, X3, X4, lesscB_in_g(X1))
U1_GA(X1, X2, X3, X4, lesscB_out_g(X1)) → U2_GA(X1, X2, X3, X4, insertA_in_ga(X2, X4))
U1_GA(X1, X2, X3, X4, lesscB_out_g(X1)) → INSERTA_IN_GA(X2, X4)
INSERTH_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U19_AGA(X1, X2, X3, X4, X5, pI_in_agga(X1, X2, X3, X5))
INSERTH_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → PI_IN_AGGA(X1, X2, X3, X5)
PI_IN_AGGA(X1, X2, X3, X4) → U12_AGGA(X1, X2, X3, X4, lessD_in_ag(X1, X2))
PI_IN_AGGA(X1, X2, X3, X4) → LESSD_IN_AG(X1, X2)
LESSD_IN_AG(s(X1), s(X2)) → U3_AG(X1, X2, lessD_in_ag(X1, X2))
LESSD_IN_AG(s(X1), s(X2)) → LESSD_IN_AG(X1, X2)
PI_IN_AGGA(X1, X2, X3, X4) → U13_AGGA(X1, X2, X3, X4, lesscD_in_ag(X1, X2))
U13_AGGA(X1, X2, X3, X4, lesscD_out_ag(X1, X2)) → U14_AGGA(X1, X2, X3, X4, insertE_in_gga(X1, X3, X4))
U13_AGGA(X1, X2, X3, X4, lesscD_out_ag(X1, X2)) → INSERTE_IN_GGA(X1, X3, X4)
INSERTE_IN_GGA(X1, tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U4_GGA(X1, X2, X3, X4, X5, lessG_in_gg(X1, X2))
INSERTE_IN_GGA(X1, tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → LESSG_IN_GG(X1, X2)
LESSG_IN_GG(s(X1), s(X2)) → U10_GG(X1, X2, lessG_in_gg(X1, X2))
LESSG_IN_GG(s(X1), s(X2)) → LESSG_IN_GG(X1, X2)
INSERTE_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U5_GGA(X1, X2, X3, X4, X5, lesscF_in_gg(X1, X2))
U5_GGA(X1, X2, X3, X4, X5, lesscF_out_gg(X1, X2)) → U6_GGA(X1, X2, X3, X4, X5, insertE_in_gga(X1, X3, X5))
U5_GGA(X1, X2, X3, X4, X5, lesscF_out_gg(X1, X2)) → INSERTE_IN_GGA(X1, X3, X5)
INSERTE_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U7_GGA(X1, X2, X3, X4, X5, lessG_in_gg(X2, s(X1)))
INSERTE_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → LESSG_IN_GG(X2, s(X1))
INSERTE_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U8_GGA(X1, X2, X3, X4, X5, lesscG_in_gg(X2, s(X1)))
U8_GGA(X1, X2, X3, X4, X5, lesscG_out_gg(X2, s(X1))) → U9_GGA(X1, X2, X3, X4, X5, insertE_in_gga(X1, X4, X5))
U8_GGA(X1, X2, X3, X4, X5, lesscG_out_gg(X2, s(X1))) → INSERTE_IN_GGA(X1, X4, X5)
INSERTH_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U20_AGA(X1, X2, X3, X4, X5, pJ_in_gaga(X2, X1, X4, X5))
INSERTH_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PJ_IN_GAGA(X2, X1, X4, X5)
PJ_IN_GAGA(X1, X2, X3, X4) → U15_GAGA(X1, X2, X3, X4, lessK_in_ga(X1, X2))
PJ_IN_GAGA(X1, X2, X3, X4) → LESSK_IN_GA(X1, X2)
LESSK_IN_GA(s(X1), s(X2)) → U11_GA(X1, X2, lessK_in_ga(X1, X2))
LESSK_IN_GA(s(X1), s(X2)) → LESSK_IN_GA(X1, X2)
PJ_IN_GAGA(X1, X2, X3, X4) → U16_GAGA(X1, X2, X3, X4, lesscK_in_ga(X1, X2))
U16_GAGA(X1, X2, X3, X4, lesscK_out_ga(X1, X2)) → U17_GAGA(X1, X2, X3, X4, insertH_in_aga(X2, X3, X4))
U16_GAGA(X1, X2, X3, X4, lesscK_out_ga(X1, X2)) → INSERTH_IN_AGA(X2, X3, X4)
INSERTH_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → U21_AGA(X1, X2, X3, X4, insertH_in_aga(s(X1), X3, X4))
INSERTH_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → INSERTH_IN_AGA(s(X1), X3, X4)
INSERTH_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U22_AGA(X1, X2, X3, X4, X5, lessK_in_ga(X2, X1))
INSERTH_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → LESSK_IN_GA(X2, X1)
INSERTH_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U23_AGA(X1, X2, X3, X4, X5, lesscK_in_ga(X2, X1))
U23_AGA(X1, X2, X3, X4, X5, lesscK_out_ga(X2, X1)) → U24_AGA(X1, X2, X3, X4, X5, insertH_in_aga(s(X1), X4, X5))
U23_AGA(X1, X2, X3, X4, X5, lesscK_out_ga(X2, X1)) → INSERTH_IN_AGA(s(X1), X4, X5)

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))
lesscD_in_ag(0, s(X1)) → lesscD_out_ag(0, s(X1))
lesscD_in_ag(s(X1), s(X2)) → U28_ag(X1, X2, lesscD_in_ag(X1, X2))
U28_ag(X1, X2, lesscD_out_ag(X1, X2)) → lesscD_out_ag(s(X1), s(X2))
lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
insertH_in_aga(x1, x2, x3)  =  insertH_in_aga(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
insertA_in_ga(x1, x2)  =  insertA_in_ga(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
pI_in_agga(x1, x2, x3, x4)  =  pI_in_agga(x2, x3)
lessD_in_ag(x1, x2)  =  lessD_in_ag(x2)
lesscD_in_ag(x1, x2)  =  lesscD_in_ag(x2)
lesscD_out_ag(x1, x2)  =  lesscD_out_ag(x1, x2)
U28_ag(x1, x2, x3)  =  U28_ag(x2, x3)
insertE_in_gga(x1, x2, x3)  =  insertE_in_gga(x1, x2)
lessG_in_gg(x1, x2)  =  lessG_in_gg(x1, x2)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
pJ_in_gaga(x1, x2, x3, x4)  =  pJ_in_gaga(x1, x3)
lessK_in_ga(x1, x2)  =  lessK_in_ga(x1)
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
INSERTH_IN_AGA(x1, x2, x3)  =  INSERTH_IN_AGA(x2)
U18_AGA(x1, x2, x3, x4, x5)  =  U18_AGA(x1, x2, x3, x5)
INSERTA_IN_GA(x1, x2)  =  INSERTA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)
U2_GA(x1, x2, x3, x4, x5)  =  U2_GA(x1, x2, x3, x5)
U19_AGA(x1, x2, x3, x4, x5, x6)  =  U19_AGA(x2, x3, x4, x6)
PI_IN_AGGA(x1, x2, x3, x4)  =  PI_IN_AGGA(x2, x3)
U12_AGGA(x1, x2, x3, x4, x5)  =  U12_AGGA(x2, x3, x5)
LESSD_IN_AG(x1, x2)  =  LESSD_IN_AG(x2)
U3_AG(x1, x2, x3)  =  U3_AG(x2, x3)
U13_AGGA(x1, x2, x3, x4, x5)  =  U13_AGGA(x2, x3, x5)
U14_AGGA(x1, x2, x3, x4, x5)  =  U14_AGGA(x1, x2, x3, x5)
INSERTE_IN_GGA(x1, x2, x3)  =  INSERTE_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4, x5, x6)  =  U4_GGA(x1, x2, x3, x4, x6)
LESSG_IN_GG(x1, x2)  =  LESSG_IN_GG(x1, x2)
U10_GG(x1, x2, x3)  =  U10_GG(x1, x2, x3)
U5_GGA(x1, x2, x3, x4, x5, x6)  =  U5_GGA(x1, x2, x3, x4, x6)
U6_GGA(x1, x2, x3, x4, x5, x6)  =  U6_GGA(x1, x2, x3, x4, x6)
U7_GGA(x1, x2, x3, x4, x5, x6)  =  U7_GGA(x1, x2, x3, x4, x6)
U8_GGA(x1, x2, x3, x4, x5, x6)  =  U8_GGA(x1, x2, x3, x4, x6)
U9_GGA(x1, x2, x3, x4, x5, x6)  =  U9_GGA(x1, x2, x3, x4, x6)
U20_AGA(x1, x2, x3, x4, x5, x6)  =  U20_AGA(x2, x3, x4, x6)
PJ_IN_GAGA(x1, x2, x3, x4)  =  PJ_IN_GAGA(x1, x3)
U15_GAGA(x1, x2, x3, x4, x5)  =  U15_GAGA(x1, x3, x5)
LESSK_IN_GA(x1, x2)  =  LESSK_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
U16_GAGA(x1, x2, x3, x4, x5)  =  U16_GAGA(x1, x3, x5)
U17_GAGA(x1, x2, x3, x4, x5)  =  U17_GAGA(x1, x3, x5)
U21_AGA(x1, x2, x3, x4, x5)  =  U21_AGA(x2, x3, x5)
U22_AGA(x1, x2, x3, x4, x5, x6)  =  U22_AGA(x2, x3, x4, x6)
U23_AGA(x1, x2, x3, x4, x5, x6)  =  U23_AGA(x2, x3, x4, x6)
U24_AGA(x1, x2, x3, x4, x5, x6)  =  U24_AGA(x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 27 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSK_IN_GA(s(X1), s(X2)) → LESSK_IN_GA(X1, X2)

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))
lesscD_in_ag(0, s(X1)) → lesscD_out_ag(0, s(X1))
lesscD_in_ag(s(X1), s(X2)) → U28_ag(X1, X2, lesscD_in_ag(X1, X2))
U28_ag(X1, X2, lesscD_out_ag(X1, X2)) → lesscD_out_ag(s(X1), s(X2))
lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
lesscD_in_ag(x1, x2)  =  lesscD_in_ag(x2)
lesscD_out_ag(x1, x2)  =  lesscD_out_ag(x1, x2)
U28_ag(x1, x2, x3)  =  U28_ag(x2, x3)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
LESSK_IN_GA(x1, x2)  =  LESSK_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSK_IN_GA(s(X1), s(X2)) → LESSK_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESSK_IN_GA(x1, x2)  =  LESSK_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSK_IN_GA(s(X1)) → LESSK_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• LESSK_IN_GA(s(X1)) → LESSK_IN_GA(X1)
  The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSG_IN_GG(s(X1), s(X2)) → LESSG_IN_GG(X1, X2)

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))
lesscD_in_ag(0, s(X1)) → lesscD_out_ag(0, s(X1))
lesscD_in_ag(s(X1), s(X2)) → U28_ag(X1, X2, lesscD_in_ag(X1, X2))
U28_ag(X1, X2, lesscD_out_ag(X1, X2)) → lesscD_out_ag(s(X1), s(X2))
lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
lesscD_in_ag(x1, x2)  =  lesscD_in_ag(x2)
lesscD_out_ag(x1, x2)  =  lesscD_out_ag(x1, x2)
U28_ag(x1, x2, x3)  =  U28_ag(x2, x3)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
LESSG_IN_GG(x1, x2)  =  LESSG_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSG_IN_GG(s(X1), s(X2)) → LESSG_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSG_IN_GG(s(X1), s(X2)) → LESSG_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• LESSG_IN_GG(s(X1), s(X2)) → LESSG_IN_GG(X1, X2)
  The graph contains the following edges 1 > 1, 2 > 2

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

INSERTE_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U5_GGA(X1, X2, X3, X4, X5, lesscF_in_gg(X1, X2))
U5_GGA(X1, X2, X3, X4, X5, lesscF_out_gg(X1, X2)) → INSERTE_IN_GGA(X1, X3, X5)
INSERTE_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U8_GGA(X1, X2, X3, X4, X5, lesscG_in_gg(X2, s(X1)))
U8_GGA(X1, X2, X3, X4, X5, lesscG_out_gg(X2, s(X1))) → INSERTE_IN_GGA(X1, X4, X5)

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))
lesscD_in_ag(0, s(X1)) → lesscD_out_ag(0, s(X1))
lesscD_in_ag(s(X1), s(X2)) → U28_ag(X1, X2, lesscD_in_ag(X1, X2))
U28_ag(X1, X2, lesscD_out_ag(X1, X2)) → lesscD_out_ag(s(X1), s(X2))
lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
lesscD_in_ag(x1, x2)  =  lesscD_in_ag(x2)
lesscD_out_ag(x1, x2)  =  lesscD_out_ag(x1, x2)
U28_ag(x1, x2, x3)  =  U28_ag(x2, x3)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
INSERTE_IN_GGA(x1, x2, x3)  =  INSERTE_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4, x5, x6)  =  U5_GGA(x1, x2, x3, x4, x6)
U8_GGA(x1, x2, x3, x4, x5, x6)  =  U8_GGA(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

INSERTE_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U5_GGA(X1, X2, X3, X4, X5, lesscF_in_gg(X1, X2))
U5_GGA(X1, X2, X3, X4, X5, lesscF_out_gg(X1, X2)) → INSERTE_IN_GGA(X1, X3, X5)
INSERTE_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U8_GGA(X1, X2, X3, X4, X5, lesscG_in_gg(X2, s(X1)))
U8_GGA(X1, X2, X3, X4, X5, lesscG_out_gg(X2, s(X1))) → INSERTE_IN_GGA(X1, X4, X5)

The TRS R consists of the following rules:

lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
INSERTE_IN_GGA(x1, x2, x3)  =  INSERTE_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4, x5, x6)  =  U5_GGA(x1, x2, x3, x4, x6)
U8_GGA(x1, x2, x3, x4, x5, x6)  =  U8_GGA(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(26) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

INSERTE_IN_GGA(X1, tree(X2, X3, X4)) → U5_GGA(X1, X2, X3, X4, lesscF_in_gg(X1, X2))
U5_GGA(X1, X2, X3, X4, lesscF_out_gg(X1, X2)) → INSERTE_IN_GGA(X1, X3)
INSERTE_IN_GGA(X1, tree(X2, X3, X4)) → U8_GGA(X1, X2, X3, X4, lesscG_in_gg(X2, s(X1)))
U8_GGA(X1, X2, X3, X4, lesscG_out_gg(X2, s(X1))) → INSERTE_IN_GGA(X1, X4)

The TRS R consists of the following rules:

lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

lesscF_in_gg(x0, x1)
lesscG_in_gg(x0, x1)
U45_gg(x0, x1, x2)
U33_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• U5_GGA(X1, X2, X3, X4, lesscF_out_gg(X1, X2)) → INSERTE_IN_GGA(X1, X3)
  The graph contains the following edges 1 >= 1, 5 > 1, 3 >= 2

• U8_GGA(X1, X2, X3, X4, lesscG_out_gg(X2, s(X1))) → INSERTE_IN_GGA(X1, X4)
  The graph contains the following edges 1 >= 1, 5 > 1, 4 >= 2

• INSERTE_IN_GGA(X1, tree(X2, X3, X4)) → U5_GGA(X1, X2, X3, X4, lesscF_in_gg(X1, X2))
  The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 2 > 4

• INSERTE_IN_GGA(X1, tree(X2, X3, X4)) → U8_GGA(X1, X2, X3, X4, lesscG_in_gg(X2, s(X1)))
  The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 2 > 4

(29) YES

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSD_IN_AG(s(X1), s(X2)) → LESSD_IN_AG(X1, X2)

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))
lesscD_in_ag(0, s(X1)) → lesscD_out_ag(0, s(X1))
lesscD_in_ag(s(X1), s(X2)) → U28_ag(X1, X2, lesscD_in_ag(X1, X2))
U28_ag(X1, X2, lesscD_out_ag(X1, X2)) → lesscD_out_ag(s(X1), s(X2))
lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
lesscD_in_ag(x1, x2)  =  lesscD_in_ag(x2)
lesscD_out_ag(x1, x2)  =  lesscD_out_ag(x1, x2)
U28_ag(x1, x2, x3)  =  U28_ag(x2, x3)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
LESSD_IN_AG(x1, x2)  =  LESSD_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(31) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSD_IN_AG(s(X1), s(X2)) → LESSD_IN_AG(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESSD_IN_AG(x1, x2)  =  LESSD_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(33) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSD_IN_AG(s(X2)) → LESSD_IN_AG(X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• LESSD_IN_AG(s(X2)) → LESSD_IN_AG(X2)
  The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

U1_GA(X1, X2, X3, X4, lesscB_out_g(X1)) → INSERTA_IN_GA(X2, X4)
INSERTA_IN_GA(tree(X1, X2, X3), tree(X1, X4, X3)) → U1_GA(X1, X2, X3, X4, lesscB_in_g(X1))

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))
lesscD_in_ag(0, s(X1)) → lesscD_out_ag(0, s(X1))
lesscD_in_ag(s(X1), s(X2)) → U28_ag(X1, X2, lesscD_in_ag(X1, X2))
U28_ag(X1, X2, lesscD_out_ag(X1, X2)) → lesscD_out_ag(s(X1), s(X2))
lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
lesscD_in_ag(x1, x2)  =  lesscD_in_ag(x2)
lesscD_out_ag(x1, x2)  =  lesscD_out_ag(x1, x2)
U28_ag(x1, x2, x3)  =  U28_ag(x2, x3)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
INSERTA_IN_GA(x1, x2)  =  INSERTA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(38) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(39) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

U1_GA(X1, X2, X3, X4, lesscB_out_g(X1)) → INSERTA_IN_GA(X2, X4)
INSERTA_IN_GA(tree(X1, X2, X3), tree(X1, X4, X3)) → U1_GA(X1, X2, X3, X4, lesscB_in_g(X1))

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
INSERTA_IN_GA(x1, x2)  =  INSERTA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(40) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U1_GA(X1, X2, X3, lesscB_out_g(X1)) → INSERTA_IN_GA(X2)
INSERTA_IN_GA(tree(X1, X2, X3)) → U1_GA(X1, X2, X3, lesscB_in_g(X1))

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))

The set Q consists of the following terms:

lesscB_in_g(x0)

We have to consider all (P,Q,R)-chains.

(42) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• INSERTA_IN_GA(tree(X1, X2, X3)) → U1_GA(X1, X2, X3, lesscB_in_g(X1))
  The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

• U1_GA(X1, X2, X3, lesscB_out_g(X1)) → INSERTA_IN_GA(X2)
  The graph contains the following edges 2 >= 1

(43) YES

(44) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

INSERTH_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PJ_IN_GAGA(X2, X1, X4, X5)
PJ_IN_GAGA(X1, X2, X3, X4) → U16_GAGA(X1, X2, X3, X4, lesscK_in_ga(X1, X2))
U16_GAGA(X1, X2, X3, X4, lesscK_out_ga(X1, X2)) → INSERTH_IN_AGA(X2, X3, X4)
INSERTH_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → INSERTH_IN_AGA(s(X1), X3, X4)
INSERTH_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U23_AGA(X1, X2, X3, X4, X5, lesscK_in_ga(X2, X1))
U23_AGA(X1, X2, X3, X4, X5, lesscK_out_ga(X2, X1)) → INSERTH_IN_AGA(s(X1), X4, X5)

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))
lesscD_in_ag(0, s(X1)) → lesscD_out_ag(0, s(X1))
lesscD_in_ag(s(X1), s(X2)) → U28_ag(X1, X2, lesscD_in_ag(X1, X2))
U28_ag(X1, X2, lesscD_out_ag(X1, X2)) → lesscD_out_ag(s(X1), s(X2))
lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
lesscD_in_ag(x1, x2)  =  lesscD_in_ag(x2)
lesscD_out_ag(x1, x2)  =  lesscD_out_ag(x1, x2)
U28_ag(x1, x2, x3)  =  U28_ag(x2, x3)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
INSERTH_IN_AGA(x1, x2, x3)  =  INSERTH_IN_AGA(x2)
PJ_IN_GAGA(x1, x2, x3, x4)  =  PJ_IN_GAGA(x1, x3)
U16_GAGA(x1, x2, x3, x4, x5)  =  U16_GAGA(x1, x3, x5)
U23_AGA(x1, x2, x3, x4, x5, x6)  =  U23_AGA(x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(45) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(46) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

INSERTH_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PJ_IN_GAGA(X2, X1, X4, X5)
PJ_IN_GAGA(X1, X2, X3, X4) → U16_GAGA(X1, X2, X3, X4, lesscK_in_ga(X1, X2))
U16_GAGA(X1, X2, X3, X4, lesscK_out_ga(X1, X2)) → INSERTH_IN_AGA(X2, X3, X4)
INSERTH_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → INSERTH_IN_AGA(s(X1), X3, X4)
INSERTH_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U23_AGA(X1, X2, X3, X4, X5, lesscK_in_ga(X2, X1))
U23_AGA(X1, X2, X3, X4, X5, lesscK_out_ga(X2, X1)) → INSERTH_IN_AGA(s(X1), X4, X5)

The TRS R consists of the following rules:

lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
0  =  0
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
INSERTH_IN_AGA(x1, x2, x3)  =  INSERTH_IN_AGA(x2)
PJ_IN_GAGA(x1, x2, x3, x4)  =  PJ_IN_GAGA(x1, x3)
U16_GAGA(x1, x2, x3, x4, x5)  =  U16_GAGA(x1, x3, x5)
U23_AGA(x1, x2, x3, x4, x5, x6)  =  U23_AGA(x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(47) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

INSERTH_IN_AGA(tree(X2, X3, X4)) → PJ_IN_GAGA(X2, X4)
PJ_IN_GAGA(X1, X3) → U16_GAGA(X1, X3, lesscK_in_ga(X1))
U16_GAGA(X1, X3, lesscK_out_ga(X1)) → INSERTH_IN_AGA(X3)
INSERTH_IN_AGA(tree(0, X2, X3)) → INSERTH_IN_AGA(X3)
INSERTH_IN_AGA(tree(s(X2), X3, X4)) → U23_AGA(X2, X3, X4, lesscK_in_ga(X2))
U23_AGA(X2, X3, X4, lesscK_out_ga(X2)) → INSERTH_IN_AGA(X4)

The TRS R consists of the following rules:

lesscK_in_ga(0) → lesscK_out_ga(0)
lesscK_in_ga(s(X1)) → U40_ga(X1, lesscK_in_ga(X1))
U40_ga(X1, lesscK_out_ga(X1)) → lesscK_out_ga(s(X1))

The set Q consists of the following terms:

lesscK_in_ga(x0)
U40_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(49) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• PJ_IN_GAGA(X1, X3) → U16_GAGA(X1, X3, lesscK_in_ga(X1))
  The graph contains the following edges 1 >= 1, 2 >= 2

• U16_GAGA(X1, X3, lesscK_out_ga(X1)) → INSERTH_IN_AGA(X3)
  The graph contains the following edges 2 >= 1

• INSERTH_IN_AGA(tree(X2, X3, X4)) → PJ_IN_GAGA(X2, X4)
  The graph contains the following edges 1 > 1, 1 > 2

• INSERTH_IN_AGA(tree(s(X2), X3, X4)) → U23_AGA(X2, X3, X4, lesscK_in_ga(X2))
  The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

• INSERTH_IN_AGA(tree(0, X2, X3)) → INSERTH_IN_AGA(X3)
  The graph contains the following edges 1 > 1

• U23_AGA(X2, X3, X4, lesscK_out_ga(X2)) → INSERTH_IN_AGA(X4)
  The graph contains the following edges 3 >= 1

(50) YES